$\forall$$r$:CRng. \\[0ex]IsIntegDom($r$) $\Leftarrow\!\Rightarrow$ (0 $\neq$ 1 $\in$ $\mid$$r$$\mid$ \& ($\forall$$u$, $v$:$\mid$$r$$\mid$. (($u$ $\ast$ $v$) = 0 $\in$ $\mid$$r$$\mid$) $\Rightarrow$ (($u$ = 0) $\vee$ ($v$ = 0))))